A, B:Realizer.
R-Feasible(A)
 R-Feasible(B)
 (i,j:Id
 (((x:Id. R-has-loc(A;x) = i = x  ) & (x:Id. R-has-loc(B;x) = j = x  ) & ((i = j))
 (& kdom(R-da(A;i)). 

 (& T=R-da(A;i)(k)  
 (& T(isrcv(k))
 (&  (((source(lnk(k)) = i  Id)  (T r R-da(B;destination(lnk(k)))(k)?Top))
 (&  & ((destination(lnk(k)) = i  Id)  (R-da(B;source(lnk(k)))(k)?Void r T)))))
 A || B 

latex

Definitions	P  Q, True, T, P  Q, A, x. t(x), A c B, , t  T, xdom(f). v=f(x)   P(x;v), P & Q, x:A. B(x), P  Q, Realizer, x:A. B(x), False, x(s)
Lemmas	eq id wf, R-icompat-one-loc, assert-eq-id, true wf, squash wf, R-has-loc wf, bool wf, finite-prob-space wf, decl-type wf, decl-state wf, IdLnk wf, Knd wf, rationals wf, Id wf, unit wf, R-Feasible wf, ldst wf, R-da wf, fpf-cap wf, fpf-ap wf, lnk wf, lsrc wf, isrcv wf, top wf, fpf wf, fpf-trivial-subtype-top, fpf-dom wf, assert wf, R-compat-disjoint